|
The Mizar system consists of a formal language for writing mathematical definitions and proofs, a proof assistant which is able to mechanically check proofs written in this language, and a library of formalized mathematics which can be used in the proof of new theorems. The system is maintained and developed by the Mizar Project, formerly under the direction of its founder Andrzej Trybulec. The Mizar Mathematical Library is the largest coherent body of strictly formalized mathematics in existence. == History == The Mizar Project was started around 1973 by Andrzej Trybulec as an attempt to reconstruct mathematical vernacular so it can be checked by a computer. Its current goal, apart from the continual development of the Mizar System, is the collaborative creation of a large library of formally verified proofs, covering most of the core of modern mathematics. This is in-line with the influential QED manifesto. Currently the project is developed and maintained by research groups at Białystok University, Poland, the University of Alberta, Canada, and Shinshu University, Japan. While the Mizar proof checker remains proprietary,〔(Mailing list discussion ) referring to the close-sourcing of Mizar.〕 the Mizar Mathematical Library – the sizable body of formalized mathematics that it verified – is licensed open-source.〔(Mailing list announcement ) referring to the open-sourcing of MML.〕 Papers related to the Mizar system regularly appear in the peer-reviewed journals of the mathematic formalization academic community. These include ''Studies in Logic, Grammar and Rhetoric'', ''Intelligent Computer Mathematics'', ''Interactive Theorem Proving'', ''Journal of Automated Reasoning'' and the ''Journal of Formalized Reasoning''. 抄文引用元・出典: フリー百科事典『 ウィキペディア（Wikipedia）』 ■ウィキペディアで「Mizar system」の詳細全文を読む スポンサード リンク
|